Summary

Refactors the pointer-to-integer work in #1002 into a reviewable red/green history and fixes the remaining symbolic regressions in the address model.

This PR now does four things:

• adds a focused cross-frame reproducer showing what master cannot prove today
• introduces a stable stack allocation identity for pointer casts via frameId
• fixes pointer-to-integer address computation to recover layout from the actual stack slot instead of relying only on the cast source pointee type
• promotes the pointer-cast regressions that are now fully proved from *-fail cases into normal passing prove tests

Implementation highlights:

• adds stable frame ids to the runtime configuration and stack frames
• keys <addressMap> / <exposedSet> by stable allocation identity instead of relative stack depth
• keeps lazy address allocation for pointer-to-integer casts and PointerExposeAddress
• recovers byte step and allocation layout from the referenced stack slot, which fixes ZST-wrapper and element-offset alignment cases

Commit Guide

1. test(prove): add cross-frame pointer cast reproducer
   • adds a red proof and expected output demonstrating the missing behavior on master
2. feat(rt): stabilize stack allocation identity for ptr casts
   • introduces stable frame ids and uses them for address allocation identity
3. fix(rt): recover pointer cast layout from stack slots
   • fixes byte-step / allocation-layout recovery for pointer-to-integer casts
4. test(prove): promote resolved pointer cast regressions
   • restores the original PR coverage as passing prove tests and removes obsolete *-fail expectations

Verification

Local validation run on the rewritten branch:

uv --directory kmir run pytest src/tests/integration/test_integration.py -v --timeout=600 -k 'alignment-check or interior-mut3 or local-raw or ptr-through-wrapper or ptr-transmute-nonzero or ptr-transmute-two-locals or ptr_offset or raw-ptr-cast or ref-ptr-cast-elem-offset or ref-ptr-cast-elem or ptr-cast-cross-frame-eq'

Result:

• 11 passed, 266 deselected

Additional proof checks used while validating the migrated regressions:

• raw-ptr-cast-fail, ptr-through-wrapper-fail, local-raw-fail, ref-ptr-cast-elem-offset-fail, ref-ptr-cast-elem-fail, and interior-mut3-fail now each report ProofStatus.PASSED with stuck: 0 and failing: 0, which is why they are promoted to normal pass tests in the final commit

GitHub Actions on the rewritten history are currently in progress and should be treated as the remaining readiness gate.

Related

• Closes feat: add address allocation model for pointer-to-integer semantics #1002
• Fixes Extend pointer emulation to pass alignment check #638
• Supersedes the PTR_OFFSET / alignment-block workarounds that motivated the earlier attempts